|
In lambda calculus, a branch of mathematical logic concerned with the formal study of functions, a reduction strategy is how a complex expression is reduced to a simple expression by successive reduction steps. It is similar to but subtly different from the notion of evaluation strategy in computer science. Roughly, a reduction strategy is a function that maps a lambda calculus term with reducible expressions to one particular reducible expression, the one to be reduced next. Mathematical logicians have studied the properties of this system for decades, and the superficial similarity between the description of evaluation strategies and reduction strategies originally misled programming language researchers to speculate that the two were identical, a belief that is still visible in popular textbooks from the early 1980s;〔Structure and Interpretation of Computer Science by Abelson and Sussman, MIT Press 1983〕 these are, however, different concepts. Plotkin〔Call-by-name, call-by-value, and the lambda calculus〕 showed in 1973, however, that a proper model of an evaluation strategy calls for the formulation of a new axiom for function calls, that is, an entirely new calculus. He validates this idea with two different calculi: one for call-by-name and another one for call-by-value, each for purely functional programming languages. He also shows that such a calculus satisfies two natural criteria. First, a calculus defines an evaluation function that maps closed terms (representations of programs) to answers (representations of outputs). This theorem relies on a conventional Church–Rosser theorem for the modified calculus. The evaluation function is defined via the traditional Curry–Feys standardization theorem. Second, the calculus is a sound equational reasoning system with respect to Morris's notion of observational equivalence.〔Programming languages and lambda calculus by James Morris, MIT 1968〕 Twenty years later, Crank and Felleisen showed how to scale Plotkin's work to languages with imperative assignment statements.〔Parameter-Passing and the Lambda Calculus by Crank and Felleisen, Principles of Programming Languages 1991 〕 They define calculi for a language with variables, functions, function application and assignment statement that capture the conventional notions of parameter passing and evaluation strategies of a wide array of programming languages. They show that each calculus satisfies Plotkin's criteria, including traditional Church–Rosser and Curry–Feys theorems respectively. In addition, they introduce a calculus that reifies ML's notion of reference cell. Ariola and Felleisen〔The call-by-need lambda calculus by Ariola and Felleisen, Journal of Functional Programming 1997〕 and independently Maraist, Odersky and Wadler 〔The call-by-need lambda calculus by Maraist Odersky and Wadler, Journal of Functional Programming 1999〕 completed this line of work with the design of a lambda calculus that precisely relates the notion of call-by-need aka lazy functional programming to an equational system of calculation. Unlike Plotkin's call-by-value and call-by-name calculi, this call-by-need calculus requires four axioms to characterize function calls. Chang and Felleisen〔The call-by-need lambda calculus, revisited by Chang and Felleisen, European Symposium on Programming, 2012〕 were eventually able to show how to create a by-need calculus with a single, but complex axiom. == See also == * Call-by-push-value, a semantic paradigm allowing to deal with call-by-name and call-by-value at once. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Reduction strategy (lambda calculus)」の詳細全文を読む スポンサード リンク
|